perm filename SET[EKL,SYS]5 blob
sn#825729 filedate 1986-10-09 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00003 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 useful set theory
C00006 00003 (proof setfacts)
C00013 ENDMK
C⊗;
;useful set theory
(wipe-out)
(get-proofs allp prf ekl sys)
(proof sets)
;all urelements will be S-expressions
;all S-expressions will be urelements
(decl (xv yv zv) (type: |ground|) (sort: urelement))
(decl (av bv) (type: |ground→truthval|))
(axiom |∀x.urelement x|)
(label simpinfo)
(axiom |∀xv.sexp(xv)|)
(label simpinfo)
(decl epsilon (type: |ground⊗@av→truthval|) (infixname: ε) (bindingpower: 925))
(define epsilon |∀av xv.xvεav≡av(xv)|)
(label epsilondef)
(axiom |∀av bv.(∀xv.xvεav≡xvεbv)⊃av=bv|)
(label set_extensionality)
(decl intersection (type: |@av⊗@av→@av|)
(infixname: ∩) (bindingpower: 950) (prefixname: intersection))
(define intersection |∀av bv.av∩bv=λxv.(av(xv)∧bv(xv))|)
(label interdef)
(decl union (type: |@av⊗@av→@av|)
(infixname: ∪) (bindingpower: 950) (prefixname: union))
(define union |∀av bv.av∪bv=λxv.(av(xv)∨bv(xv))|)
(label uniondef)
(decl inclusion (type: |@av⊗@av→truthval|)
(infixname: ⊂) (bindingpower: 920) (prefixname: inclusion))
(define inclusion |∀av bv.av⊂bv≡∀xv.av(xv)⊃bv(xv)|)
(label inclusiondef)
(defax emptyset |emptyset=λxv.false|)
(defax emptyp |∀av.emptyp(av)=∀xv.¬av(xv)|)
;the set of occurrences of an S-exp
(decl mkset (type: |ground→@av|))
(define mkset |∀x.mkset(x)=(λyv.yv=x)|)
(label mkset_def)
;the set of members of a list
(decl mklset (type: |ground→@av|))
(define mklset |∀u.mklset(u)=λx.member(x,u)|)
(label mklsetdef)
(proof setfacts)
(axiom |∀u y.member(y,u)⊃mkset(y)⊂mklset u|)
(label mkset_mklset)
(axiom |∀av bv.av⊂bv∧bv⊂av⊃av=bv|)
(label double_inclusion)
(save-proofs set)